Exercise (Week 4)
Table of Contents
DUE: Thu 30 June 09:10:00
1 Quickcheck and Nub (9 Marks)
Download the exercise tarball and extract it to a directory in your
home directory at CSE. This tarball contains a file, called Ex03.hs,
wherein you will do all of your programming.
To test your code, run the following shell commands to open a GHCi session:
$ 3141
newclass starting new subshell for class COMP3141...
$ cabal repl
Resolving dependencies...
Configuring Ex03-1.0...
Preprocessing executable 'Ex03' for Ex03-1.0..
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Ex03 (Ex03.hs, interpreted)
Ok, one module loaded.
*Ex03>
Note that you will only need to submit Ex03.hs, so only make changes
to that file.
Download the exercise tarball and extract it to a directory on
your local machine. This tarball contains a file, called Ex03.hs,
wherein you will do all of your programming.
To test your code, run the following shell commands to open a GHCi session:
$ stack repl
Configuring GHCi with the following packages: Ex03
Using main module: 1. Package 'Ex03' component exe:Ex03 ...
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Ex03 (Ex03.hs, interpreted)
Ok, one module loaded.
*Ex03>
Note that you will only need to submit Ex03.hs, so only make changes
to that file.
As we discussed in this week's lecture, the more laws we can identify in advance, the larger our test suite will be, and the more implementation bugs it will catch - even if our tests do not, in themselves, guarantee full correctness.
The current exercise aims to explore this phenomenon.
Recall that the nub function removes duplicate elements from a list,
keeping only the first occurrence of each element.
The equations below (restated in Ex03.hs) define six algebraic
properties that the nub function satisfies.
nub (nub xs) == nub xs nub (x : nub xs) == nub (x : xs) nub (xs ++ nub ys) == nub (xs ++ ys) nub (x : x : xs) == nub (x : xs) nub (xs ++ [x] ++ xs) == nub (xs ++ [x]) nub [x] == [x]
The moral here is that, when combined with other functions, even simple functions can give rise to very rich algebraic (that is, equational) theories. Such properties are easy to think up, even without a working implementation of nub. However, as we will see, it's not all that easy to come up with an incorrect implementation of nub, one that fails only some of these properties. This is similar to the dodgy sort functions you implemented in Practical 3.
1.1 Task 1 (2 marks)
Your first task is to define a function dnub1236, which satisfies equations
1, 2, 3 and 6 above (for all x, xs and ys), but not equations 4 and 5.
That is, the equations
dnub1236 (dnub1236 xs) == dnub1236 xs dnub1236 (x : dnub1236 xs) == dnub1236 (x : xs) dnub1236 (xs ++ dnub1236 ys) == dnub1236 (xs ++ ys) dnub1236 [x] == [x]
should always hold, while the equations
dnub1236 (x : x : xs) == dnub1236 (x : xs) dnub1236 (xs ++ [x] ++ xs) = dnub1236 (xs ++ [x])
should fail for at least one x and xs. To show that this is the case,
define such a failing pair (x,xs) for each equation, in dnub1236_c4 and
dnub1236_c5.
1.2 Task 2 (2 marks)
Implement a similar dodgy nub function, dnub12345, which fails only
equation 6. For the sixth equation, construct a failing input in dnub12345_c6.
1.3 Task 3 (2 marks)
Implement one more dodgy nub function, this time one that satisfies 4,5,6, but not 1,2,3.
1.4 Task 4 (3 marks)
Finally, show that six equations do not guarantee full correctness for nub: construct
a function dnub123456 which satisfies all six properties, and yet behaves differently
from the nub function on at least one input. Exhibit such an input in dnub123456_c.
Hint
Your implementations don't have to resemble the real nub function, as long as they pass the tests they are supposed to pass, and fail the tests they are supposed to fail.
Remark
Although Task 4 should not be too challenging, notice that even these six simple equations eliminate
quite a large number of possible incorrect implementations of the nub function. Haskell's powerful type system
eliminates others: for example, the function f xs = sort (nub xs) satisfies all six
equations, but is trivially rejected due to a type class mismatch.
If you're looking for a real challenge, try implementing a dodgy nub function that satisfies all 6
equations above, along with the property elem x xs ==> elem x (nub xs).
1.5 Submission instructions
You can submit your exercise by typing:
$ give cs3141 ex03 Ex03.hs
on a CSE terminal, or by using the give web interface. Your file must be named Ex03.hs (case-sensitive!).
A dry-run test will partially autotest your solution at submission time. To get full marks, you will need to perform further testing yourself.